$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ prior($X$))) $\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. ((${\it e'}$ $<$loc $e$) \& ($\uparrow$(${\it e'}$ $\in_{b}$ $X$))))